Step of Proof: wellfounded_wf
9,38
postcript
pdf
Inference at
*
I
of proof for Lemma
wellfounded
wf
:
A
:Type,
r
:(
A
A
). WellFnd{i}(
A
;
x
,
y
.
r
(
x
,
y
))
'
latex
by ((Unfold `wellfounded` 0)
CollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 1:n
C
),(first_nat 3:n)) (first_tok :t) inil_term)))
latex
C
.
Definitions
x
(
s
)
,
P
Q
,
x
(
s1
,
s2
)
,
WellFnd{i}(
A
;
x
,
y
.
R
(
x
;
y
))
,
t
T
,
,
x
:
A
.
B
(
x
)
Lemmas
guard
wf
origin